\begin{tabbing}
$\forall$${\it es}$:ES, $T$:Type, $I$:MaInterface($T$), $l$:IdLnk, ${\it tg}$:Id.
\\[0ex]ma{-}interface{-}consistent2(${\it es}$;$I$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\\[0ex]$\Rightarrow$ (source($l$) $\in$ ma{-}interface{-}locs($I$))
\\[0ex]$\Rightarrow$ only events in ma{-}interface{-}dom($I$;source($l$)) send on $l$ with ${\it tg}$
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd.\+
\\[0ex]($k$ $\in$ ma{-}interface{-}dom($I$;source($l$)))
\\[0ex]$\Rightarrow$ \=$k$(v:ma{-}interface{-}valtype($I$;source($l$);$k$)) sends on $l$ [${\it tg}$:$T$, $\lambda$$p$.let $s$,$v$ = $p$\+
\\[0ex]in
\\[0ex]ma{-}interface{-}code($I$;source($l$);$k$)($s$,$v$) $<$state, v$>$]?[])
\-\-\\[0ex]$\Rightarrow$ glued(${\it es}$; $T$; ($\lambda$$e$.[[$I$$\mid$source($l$)]]($e$)); [[$I$$\mid$source($l$)]]; es{-}in{-}port(${\it es}$;$l$;${\it tg}$))
\end{tabbing}